#include "Formule.hpp"
#include <iostream>
#include <sstream>

string operateur2string(operateur op) {
  switch (op) {
  case o_variable:
    return "var";
  case o_non:
    return "~";
  case o_et:
    return "/\\";
  case o_ou:
    return "\\/";
  case o_implique:
    return "=>";
  case o_equivaut:
    return "<=>";
  }
}

string formule2string(formule * f) {
  switch (f->op) {
  case o_variable:
    return *(f->nom);
  case o_non:
    return "~" + formule2string(f->arg);
  case o_et:
  case o_ou:
  case o_equivaut:
  case o_implique:
    return "("+formule2string(f->arg1)
      +" "+operateur2string(f->op)+" "
      +formule2string(f->arg2)+")";
  }
}

bool is_binary(operateur op) {
  switch (op) {
  case o_et:
  case o_ou:
  case o_equivaut:
  case o_implique:
    return true;
  default:
    return false;
  }
}

int priority_level(operateur op) {
  switch (op) {
  case o_variable:
    return -1;
  case o_non:
    return 1;
  case o_et:
    return 2;
  case o_ou:
    return 3;
  case o_implique:
    return 4;
  case o_equivaut:
    return 5;
  }
}

operateur operateur_for_level(int lvl) {
  switch (lvl) {
  case 1:
    return o_non;
  case 2:
    return o_et;
  case 3:
    return o_ou;
  case 4:
    return o_implique;
  case 5:
    return o_equivaut;
  default:
    return o_variable;
  }
}

formule * var(string * nom) {
  formule*res = new formule();
  res->op = o_variable;
  res->nom = nom;
  return res;
}

formule * var(string nom)  {
  formule*res = new formule();
  res->op = o_variable;
  res->nom = new string(nom);
  return res;
}

formule * non(formule * arg) {
  formule * res = new formule();
  res->op = o_non;
  res->arg = arg;
  return res;
}

formule * mkbinop(operateur op, formule* arg1, formule* arg2) {
  formule*res = new formule();
  res->op = op;
  res->arg1 = arg1;
  res->arg2 = arg2;
  return res;
}

formule * et(formule* arg1, formule* arg2) {
  return mkbinop(o_et,arg1,arg2);
}

formule * ou(formule* arg1, formule* arg2) {
  return mkbinop(o_ou,arg1,arg2);
}

formule * impl(formule* arg1, formule* arg2) {
  return mkbinop(o_implique,arg1,arg2);
}

formule * equiv(formule* arg1, formule* arg2) {
  return mkbinop(o_equivaut,arg1,arg2);
}

void afficherMap(map<string,int> correspondance)
{
    cout << "Votre map : " << endl;

  std::map<std::string,int>::const_iterator
   mit (correspondance.begin()),
    mend(correspondance.end());
  for(;mit!=mend;++mit) std::cout << mit->first << '\t' << mit->second <<
  std::endl;
}

map<string, int> numerote(formule * f,map<string, int> correspondance)
{
   if(is_binary(f->op))
    {
        correspondance=numerote(f->arg1,correspondance);
        correspondance=numerote(f->arg2,correspondance);
    }
    else
    {
        map<string,int>::iterator it;


	      if(f->op==o_variable)
            {

                it=correspondance.find("~"+*f->nom);
                if(it!=correspondance.end())
                {

                    correspondance[*f->nom]=-correspondance["~"+*f->nom];
                }
                else
                {
                    if(correspondance.count(*(f->nom)) == 0)
                    {

                        correspondance[*f->nom]=correspondance.size();
                    }
                }

            }
        else
		{
		  it=correspondance.find(*f->arg->nom);
		  if(it!=correspondance.end())
		    {

		      correspondance["~"+*f->arg->nom]=-correspondance[*f->arg->nom];
		    }
		  else
		    {
		        if(correspondance.count("~"+*f->arg->nom)==0)
		        {
                    correspondance["~"+*f->arg->nom]=-correspondance.size();
                }
		    }

		}
    }
    return correspondance;

}


formule * supprimerImplication(formule * f)
{
    if(is_binary(f->op))
    {
        if(operateur2string(f->op) == "=>")
        {
            f->op = o_ou;
            f->arg1=non(f->arg1);
        }
        supprimerImplication(f->arg1);
        supprimerImplication(f->arg2);
    }
    if(f->op == o_non && f->arg->op != o_variable)
    {
        supprimerImplication(f->arg);
    }
    return f;
}

formule * supprimerEquivalence(formule * f)
{
    if(is_binary(f->op))
    {
        if(operateur2string(f->op) == "<=>")
        {
            formule * formuleGauche = new formule();
            formule * formuleDroite = new formule();

            formuleGauche->op = o_implique;
            formuleGauche->arg1=f->arg1;
            formuleGauche->arg2=f->arg2;

            formuleDroite->op = o_implique;
            formuleDroite->arg1=f->arg2;
            formuleDroite->arg2=f->arg1;

            f->op=o_et;
            f->arg1=formuleGauche;
            f->arg2=formuleDroite;


        }
        supprimerEquivalence(f->arg1);
        supprimerEquivalence(f->arg2);
    }
     if(f->op == o_non && f->arg->op != o_variable)
    {
        supprimerEquivalence(f->arg);
    }
    return f;
}
